Nuprl Definition : es-real
11,40
postcript
pdf
es-real{i:l}(
es
.
P
(
es
)) ==
R
:es_realizer{i:l}. R-realizes{i:l}(
R
;
es
.
P
(
es
))
latex
Definitions
R-realizes{i:l}(
R
;
es
.
P
(
es
))
,
es_realizer{i:l}
,
x
:
A
.
B
(
x
)
FDL editor aliases
es-real
origin